#ifndef Formule
#define Formule
#include <string>
#include <vector>
#include <map>

using namespace std;

enum operateur {
  o_variable,
  o_non,
  o_et,
  o_ou,
  o_implique,
  o_equivaut
};

struct formule {
  operateur op;
  union {
    string * nom;
    struct {
      formule * arg1;
      formule * arg2;
    };
    formule * arg;
  };
};

extern formule * var(string * nom);
extern formule * var(string nom);
extern formule * non(formule * arg);
extern formule * et(formule* arg1, formule* arg2);
extern formule * ou(formule* arg1, formule* arg2);
extern formule * impl(formule* arg1, formule* arg2);
extern formule * equiv(formule* arg1, formule* arg2);

extern string operateur2string(operateur op);
extern string formule2string(formule * f);
extern bool is_binary(operateur);
extern int priority_level(operateur);
extern operateur operateur_for_level(int lvl);
extern map<string, int> numerote(formule * f,map<string, int> correspondance);
extern formule * supprimerImplication(formule * f);
extern void afficherMap(map<string,int> correspondance);
extern formule * supprimerEquivalence(formule * f);
#define START_LVL 5

// Fichiers dimacs
struct dimacs {
  int maxVar;
  vector<vector<int>*>* clauses;
};

#endif

